Nuprl Lemma : manames-overlap-case_wf
11,40
postcript
pdf
T
:Type,
x
,
y
:
T
,
nms1
,
nms2
:(MaName List). if
nms1
and
nms2
overlap then
x
else
y
fi
T
latex
Definitions
Type
,
t
T
,
MaName
,
type
List
,
x
:
A
.
B
(
x
)
,
l_disjoint(
T
;
l1
;
l2
)
,
Dec(
P
)
,
x
:
A
B
(
x
)
,
decidable
l
disjoint
manames
,
f
(
a
)
,
x
.
t
(
x
)
,
if
p
:
P
then
A
(
p
) else
B
fi
,
if
nms1
and
nms2
overlap then
x
else
y
fi
Lemmas
branch
wf
,
decidable
l
disjoint
manames
,
decidable
wf
,
l
disjoint
wf
,
MaName
wf
origin
T:Type, x, y:T, nms1, nms2:(MaName List). if nms1 and nms2 overlap then x else y fi 
T T:Type, x, y:T, nms1, nms2:(MaName List). if nms1 and nms2 overlap then x else y fi T 
B(x)
x. t(x)